The present disclosure relates to model checking in general, and to generation of a model to be utilized in model checking in particular.
Computerized devices control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a testing phase in which the bugs should be discovered. The testing phase is considered one of the most difficult tasks in developing a computerized device. Many developers of computerized devices devote a significant portion, such as 70%, of the development cycle to discover erroneous behaviors of the computerized device, also referred to as a target computerized system. The target computerized system may comprise hardware, software, firmware, a combination thereof and the like.
One known quality assurance technique is formal verification using a model checker. A model, which corresponds to the target computerized system, also referred to as a design, defines a set of variables and their respective behavior based upon each other and inputs from an environment. The model may be described by a state-machine. In some cases, a constraint, also referred to as an assumption, may be defined to limit the model. The constraint may define a property that must be held by every legal behavior of the design and the environment. A behavior of the design and the environment may be described by a set of consecutive states and a legal behavior may be a behavior that is associated with a set of consecutive states, where each state holds the constraint. The constraint may be utilized to specify the environment in which the design operates in. For example, the environment may provide an input in each cycle that is different than the previous cycle. Additionally, the constraint may be utilized to limit a portion of the design itself, such as for example determining that a specific state or set of states may never be reached by the design. Using constraints for specifying the environment or model may be more convenient or readable. Moreover, it may be less error-prone than describing a full state-machine of the environment or model manually.
As is known in the art, for example in GEIST et al., Supporting SAT based BMC on Finite Path Models, Electronic Notes in Theoretical Computer Science 144 (2006) 67-77, any path in a model can always be extended to include an additional successive state to the last state of the path. Each such path is referred to as an “infinite path”. However, when a constraint is introduced, a finite path may be induced due to the constraint. In the present disclosure, a “finite path with respect to a constraint” is an infinite path in the model that is induced by the constraint to be finite path. Such infinite path comprises a state that all its possible successive states according to the model are in violation of the constraint and therefore is induced to be a dead-end state. The finite path always comprises a dead-end state as its terminal state of the path.